| Definitions | Id, Type, Void, f(x)?z, Knd, lnk-decl(l;dt), KindDeq, f  g, rcv(l,tg), t  T, x:A  B(x),  x:A. B(x), IdDeq,  x.A(x),  x. t(x), S  T, DeclaredType(ds;x), Case b of inl(x)  s(x) ; inr(y) t(y), if b t else f fi,  b,  A, b,  , s = t, Prop, x : v,  x:A. B(x), Top, x dom(f), P  Q, x:A B(x), P & Q, P  Q, Unit, left+right, a:A fp B(a), Valtype(da;k), State(ds), State(ds), , only members of L read x, MsgA, a = b, k sends only on links in L, k affects only members of L, S  T, (with ds: ds action a:T precondition a(v) is P s v), type List, with declarations ds:dsda:dak(v) sends f s v on link l, source(l), with declarations ds:dsda:daeffect of k(v) is x := f s v, only L sends on (l with tg), only members of L affect x :t, x : t initially x = v, @i: only members of L read x, es realizer ind Rrframe compseq tag def, @i: A, R-base-ma(R), R-loc(R), [[R]], Dsys, @i: k sends only links in L, es realizer ind Rbframe compseq tag def, @i: k affects only members of L, es realizer ind Raframe compseq tag def, @i (with ds: ds action a:T precondition a(v) is P s v), es realizer ind Rpre compseq tag def, @i: with declarations ds:dsda:da k(v) sends f s v on link l, es realizer ind Rsends compseq tag def, @i: with declarations ds:dsda:daeffect of k(v) is x := f s v, es realizer ind Reffect compseq tag def, @i: only L sends on (l with tg), es realizer ind Rsframe compseq tag def, @i: only L affects x : t, es realizer ind Rframe compseq tag def, @i: x:T initially x = v, es realizer ind Rinit compseq tag def, False, True, @loc: only members of L read x, R-Feasible(R), @loc: k sends only on links in L, @loc: k writes only members of L, @loc precondition for a(v:T):P State(ds) v, sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc effect knd(v:T) x := f State(ds) v , only events in L send on lnk with tag, @loc only events in L change x:T, @loc x initially v:T, left right,  , Rnone?(x1), Rplus?(x1), es realizer ind Rplus compseq tag def, es realizer ind Rnone compseq tag def, IdLnk, rec(x.A(x)), Realizer, P Q, <a,b>, lnk(k), tag(k), isrcv(k),  T, {T}, SQType(T), s ~ t |
| Lemmas | fpf-single-dom, lnk-decl-cap, subtype rel self, Knd sq, squash wf, assert-eq-lnk, es realizer wf, unit wf, IdLnk wf, Rnone wf, Rplus wf, Rinit wf, Rframe wf, Rsframe wf, Reffect wf, Rsends wf, Rpre wf, Raframe wf, Rbframe wf, R-Feasible wf, Rrframe wf, true wf, false wf, ma-single-init wf, ma-single-frame wf, ma-single-sframe wf, ma-single-effect wf, lsrc wf, ma-single-sends wf, ma-valtype wf, fpf-join wf, decl-type wf, ma-single-pre wf, decl-state wf, ma-single-aframe wf, ma-single-bframe wf, ifthenelse wf, eq id wf, msga wf, ma-single-rframe wf, ma-empty wf, ma-state wf, fpf-cap-single1, fpf-cap-single-join, fpf-join-cap-sq, fpf-trivial-subtype-top, lnk-decl wf, fpf wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, Kind-deq wf, fpf-single wf, top wf, Knd wf, rcv wf, bool wf, bnot wf, not wf, assert wf, fpf-cap wf, Id wf, id-deq wf |